\begin{tabbing} sumdeq($a$;$b$)($p$,$q$) \\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=Case $p$ of\+ \\[0ex]inl(${\it pa}$) $\Rightarrow$ Case $q$ of inl(${\it qa}$) $\Rightarrow$ 1of($a$)(${\it pa}$,${\it qa}$) ; inr(${\it qb}$) $\Rightarrow$ false$_{2}$ \\[0ex]inr(${\it pb}$) $\Rightarrow$ Case $q$ of inl(${\it qa}$) $\Rightarrow$ false$_{2}$ ; inr(${\it qb}$) $\Rightarrow$ 1of($b$)(${\it pb}$,${\it qb}$) \- \end{tabbing}